Nuprl Lemma : R-Feasible-Rplus
11,40
postcript
pdf
A
,
B
:top.
sqequal(R-Feasible{i:l}
sqequal(R-Feasible
(Rplus(
A
;
B
));
sqequal(
(R-Feasible{i:l}(
A
)
R-Feasible{i:l}(
B
)
R-compat{i:l}(
A
;
B
)))
latex
Definitions
t
T
,
R-Feasible{i:l}(
R
)
,
x
:
A
.
B
(
x
)
Lemmas
top
wf
origin
A,B:top.
R-Feasible{i:l}(B) R-compat{i:l}(A; B))) A,B:top.
R-Feasible{i:l}(B) R-compat{i:l}(A; B))) 
Tx:A. B(x)